Formelt system

Der er ingen kildehenvisninger i denne artikel, hvilket er et problem. Begrundelsen kan findes på diskussionssiden eller i artikelhistorikken. Du kan hjælpe ved at angive kilder til de påstande, der fremføres. Hvis ikke der tilføjes kilder, vil artiklen muligvis blive slettet (marts 2018) (Lær hvordan og hvornår man kan fjerne denne skabelonbesked)

Et formelt system er et system af påstande og regler, hvor man af påstandene ved hjælp af reglerne kan udlede en række sandheder.^[1] Formelle systemer finder typisk anvendelse i studiet af de fundamentale spilleregler for logik, matematik og datalogi. Indenfor matematikken kaldes påstandene for aksiomer, reglerne kaldes slutningsregler og sandhederne kaldes sætninger.

Graden af formalisme kan variere. I de mest formelle formelle systemer tænkes alle sandheder at kunne udledes (i princippet) ved at en relativt simpel datamaskine anvender reglerne på påstandene. Et sådant formelt system skrevet i et formelt sprog består af netop disse 4 elementer

1. En endelig mængde af tegn (ofte kaldet "alfabetet")
2. En grammatik (eller syntaks) der beskriver hvordan tegnene fra (1) kan sammensættes til velformede sætninger
3. En endelig mængde af påstande - hver påstand skal bestå af tegn fra (1) og opfylde (2)
4. En mængde af regler hvormed nye velformede sætninger kan udledes af eksisterende velformede sætninger

Indtil 1930'erne regnede mange matematikere med at der kunne opstilles ét (omfattende) formelt system der kunne beskrive al matematisk viden: At det blot var et spørgsmål om af specificere den rette mængde af påstande og de rette regler, og så ville al matematisk viden så at sige kunne udledes herved. Og i 1910-1913 udgav matematikerne Alfred North Whitehead og Bertrand Russell deres storværk Principia Mathematica der tilsyneladende bekræftede dette, og var et forsøg på at definere netop en sådan mængde af påstande.

I 1931 publicerede matematikeren Kurt Gödel imidlertid sin ufuldstændighedssætning hvormed han beviste at et sådant system ikke kunne eksistere, eller mere præcist at et formelt system med indre konsistens (dvs. hvor man ikke kan udlede modstridende sandheder) ikke ville kunne definere alle matematiske sandheder ud fra en endelig mængde af påstande.^[1]

Dette bevis betød at jagten på én komplet mængde af matematiske basis-påstande kunne indstilles, men det betød ikke at formelle systemer mistede deres relevans. Dels bruges (mere eller mindre) formelle systemer generelt i matematik, men blot inden for enkelte områder, dels har formelle systemer stadig betydning i studiet af matematikkens grundelementer og dels kom de til at spille en betydelig rolle indenfor et nyt fagområde der var ved at opstå, datalogien. Brugen af og studiet af formelle systemer endvidere tæt koblet med brugen af og studiet af formelle sprog.

1. ^ ^{a b} A. G. Hamilton, Logic for Mathematicians, Cambridge University Press, ISBN 9780521368650